Termination of the given JBC could be proven:

0 JBC
↳1 JBC2FIG (⇐)
↳2 FIGraph
↳3 FIGtoITRSProof (⇐)
↳4 AND
    ↳5 ITRS
        ↳6 ITRStoIDPProof (⇔)
        ↳7 IDP
        ↳8 UsableRulesProof (⇔)
        ↳9 IDP
        ↳10 ItpfGraphProof (⇔)
        ↳11 IDP
        ↳12 IDPNonInfProof (⇐)
        ↳13 AND
            ↳14 IDP
                ↳15 IDPNonInfProof (⇐)
                ↳16 AND
                    ↳17 IDP
                        ↳18 IDPNonInfProof (⇐)
                        ↳19 AND
                            ↳20 IDP
                                ↳21 IDependencyGraphProof (⇔)
                                ↳22 TRUE
                            ↳23 IDP
                                ↳24 IDependencyGraphProof (⇔)
                                ↳25 TRUE
                    ↳26 IDP
                        ↳27 IDependencyGraphProof (⇔)
                        ↳28 TRUE
            ↳29 IDP
                ↳30 IDependencyGraphProof (⇔)
                ↳31 TRUE
    ↳32 ITRS
        ↳33 ITRStoIDPProof (⇔)
        ↳34 IDP
        ↳35 UsableRulesProof (⇔)
        ↳36 IDP
        ↳37 ItpfGraphProof (⇔)
        ↳38 IDP
        ↳39 IDPNonInfProof (⇐)
        ↳40 AND
            ↳41 IDP
                ↳42 IDependencyGraphProof (⇔)
                ↳43 TRUE
            ↳44 IDP
                ↳45 IDependencyGraphProof (⇔)
                ↳46 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
No human-readable program information known.

Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: Convert

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 283 nodes with 2 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Complex Obligation (AND)

(5) Obligation:

ITRS problem:

The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load1852(java.lang.Object(IntList(o1725, i453)), i183, i451) → Cond_Load1852(i453 > 0 && i451 + 1 > 0, java.lang.Object(IntList(o1725, i453)), i183, i451)
Cond_Load1852(TRUE, java.lang.Object(IntList(o1725, i453)), i183, i451) → Load1852(java.lang.Object(IntList(o1725, i453 - 1)), i183, i451 + 1)
Load1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) → Cond_Load18521(i454 <= 0, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451)
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) → Load1852(java.lang.Object(IntList(o1731Field0, o1731Field1)), i183, i451 * i183)
Load1852(java.lang.Object(IntList(NULL, i454)), i183, i451) → Cond_Load18522(i454 <= 0, java.lang.Object(IntList(NULL, i454)), i183, i451)
Cond_Load18522(TRUE, java.lang.Object(IntList(NULL, i454)), i183, i451) → Load1852(NULL, i183, i451)
The set Q consists of the following terms:
Load1852(java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load1852(TRUE, java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)
Cond_Load18522(TRUE, java.lang.Object(IntList(NULL, x0)), x1, x2)

(6) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


The ITRS R consists of the following rules:
Load1852(java.lang.Object(IntList(o1725, i453)), i183, i451) → Cond_Load1852(i453 > 0 && i451 + 1 > 0, java.lang.Object(IntList(o1725, i453)), i183, i451)
Cond_Load1852(TRUE, java.lang.Object(IntList(o1725, i453)), i183, i451) → Load1852(java.lang.Object(IntList(o1725, i453 - 1)), i183, i451 + 1)
Load1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) → Cond_Load18521(i454 <= 0, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451)
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) → Load1852(java.lang.Object(IntList(o1731Field0, o1731Field1)), i183, i451 * i183)
Load1852(java.lang.Object(IntList(NULL, i454)), i183, i451) → Cond_Load18522(i454 <= 0, java.lang.Object(IntList(NULL, i454)), i183, i451)
Cond_Load18522(TRUE, java.lang.Object(IntList(NULL, i454)), i183, i451) → Load1852(NULL, i183, i451)

The integer pair graph contains the following rules and edges:
(0): LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(i453[0] > 0 && i451[0] + 1 > 0, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
(1): COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], i453[1] - 1)), i183[1], i451[1] + 1)
(2): LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(i454[2] <= 0, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
(3): COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], i451[3] * i183[3])
(4): LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(i454[4] <= 0, java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])
(5): COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5]) → LOAD1852(NULL, i183[5], i451[5])

(0) -> (1), if ((java.lang.Object(IntList(o1725[0], i453[0])) →* java.lang.Object(IntList(o1725[1], i453[1])))∧(i451[0] →* i451[1])∧(i453[0] > 0 && i451[0] + 1 > 0 →* TRUE)∧(i183[0] →* i183[1]))


(1) -> (0), if ((i183[1] →* i183[0])∧(i451[1] + 1 →* i451[0])∧(java.lang.Object(IntList(o1725[1], i453[1] - 1)) →* java.lang.Object(IntList(o1725[0], i453[0]))))


(1) -> (2), if ((i183[1] →* i183[2])∧(java.lang.Object(IntList(o1725[1], i453[1] - 1)) →* java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])))∧(i451[1] + 1 →* i451[2]))


(1) -> (4), if ((java.lang.Object(IntList(o1725[1], i453[1] - 1)) →* java.lang.Object(IntList(NULL, i454[4])))∧(i183[1] →* i183[4])∧(i451[1] + 1 →* i451[4]))


(2) -> (3), if ((i183[2] →* i183[3])∧(i454[2] <= 0 →* TRUE)∧(i451[2] →* i451[3])∧(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])) →* java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3]))))


(3) -> (0), if ((java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])) →* java.lang.Object(IntList(o1725[0], i453[0])))∧(i451[3] * i183[3] →* i451[0])∧(i183[3] →* i183[0]))


(3) -> (2), if ((i183[3] →* i183[2])∧(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])) →* java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])))∧(i451[3] * i183[3] →* i451[2]))


(3) -> (4), if ((i451[3] * i183[3] →* i451[4])∧(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])) →* java.lang.Object(IntList(NULL, i454[4])))∧(i183[3] →* i183[4]))


(4) -> (5), if ((i451[4] →* i451[5])∧(i183[4] →* i183[5])∧(java.lang.Object(IntList(NULL, i454[4])) →* java.lang.Object(IntList(NULL, i454[5])))∧(i454[4] <= 0 →* TRUE))


(5) -> (0), if ((i451[5] →* i451[0])∧(NULL →* java.lang.Object(IntList(o1725[0], i453[0])))∧(i183[5] →* i183[0]))


(5) -> (2), if ((NULL →* java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])))∧(i183[5] →* i183[2])∧(i451[5] →* i451[2]))


(5) -> (4), if ((i183[5] →* i183[4])∧(i451[5] →* i451[4])∧(NULL →* java.lang.Object(IntList(NULL, i454[4]))))



The set Q consists of the following terms:
Load1852(java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load1852(TRUE, java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)
Cond_Load18522(TRUE, java.lang.Object(IntList(NULL, x0)), x1, x2)

(8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(i453[0] > 0 && i451[0] + 1 > 0, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
(1): COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], i453[1] - 1)), i183[1], i451[1] + 1)
(2): LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(i454[2] <= 0, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
(3): COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], i451[3] * i183[3])
(4): LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(i454[4] <= 0, java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])
(5): COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5]) → LOAD1852(NULL, i183[5], i451[5])

(0) -> (1), if ((java.lang.Object(IntList(o1725[0], i453[0])) →* java.lang.Object(IntList(o1725[1], i453[1])))∧(i451[0] →* i451[1])∧(i453[0] > 0 && i451[0] + 1 > 0 →* TRUE)∧(i183[0] →* i183[1]))


(1) -> (0), if ((i183[1] →* i183[0])∧(i451[1] + 1 →* i451[0])∧(java.lang.Object(IntList(o1725[1], i453[1] - 1)) →* java.lang.Object(IntList(o1725[0], i453[0]))))


(1) -> (2), if ((i183[1] →* i183[2])∧(java.lang.Object(IntList(o1725[1], i453[1] - 1)) →* java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])))∧(i451[1] + 1 →* i451[2]))


(1) -> (4), if ((java.lang.Object(IntList(o1725[1], i453[1] - 1)) →* java.lang.Object(IntList(NULL, i454[4])))∧(i183[1] →* i183[4])∧(i451[1] + 1 →* i451[4]))


(2) -> (3), if ((i183[2] →* i183[3])∧(i454[2] <= 0 →* TRUE)∧(i451[2] →* i451[3])∧(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])) →* java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3]))))


(3) -> (0), if ((java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])) →* java.lang.Object(IntList(o1725[0], i453[0])))∧(i451[3] * i183[3] →* i451[0])∧(i183[3] →* i183[0]))


(3) -> (2), if ((i183[3] →* i183[2])∧(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])) →* java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])))∧(i451[3] * i183[3] →* i451[2]))


(3) -> (4), if ((i451[3] * i183[3] →* i451[4])∧(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])) →* java.lang.Object(IntList(NULL, i454[4])))∧(i183[3] →* i183[4]))


(4) -> (5), if ((i451[4] →* i451[5])∧(i183[4] →* i183[5])∧(java.lang.Object(IntList(NULL, i454[4])) →* java.lang.Object(IntList(NULL, i454[5])))∧(i454[4] <= 0 →* TRUE))


(5) -> (0), if ((i451[5] →* i451[0])∧(NULL →* java.lang.Object(IntList(o1725[0], i453[0])))∧(i183[5] →* i183[0]))


(5) -> (2), if ((NULL →* java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])))∧(i183[5] →* i183[2])∧(i451[5] →* i451[2]))


(5) -> (4), if ((i183[5] →* i183[4])∧(i451[5] →* i451[4])∧(NULL →* java.lang.Object(IntList(NULL, i454[4]))))



The set Q consists of the following terms:
Load1852(java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load1852(TRUE, java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)
Cond_Load18522(TRUE, java.lang.Object(IntList(NULL, x0)), x1, x2)

(10) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

(11) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(i453[0] > 0 && i451[0] + 1 > 0, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
(1): COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], i453[1] - 1)), i183[1], i451[1] + 1)
(2): LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(i454[2] <= 0, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
(3): COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], i451[3] * i183[3])
(4): LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(i454[4] <= 0, java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])
(5): COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5]) → LOAD1852(NULL, i183[5], i451[5])

(0) -> (1), if (((o1725[0] →* o1725[1])∧(i453[0] →* i453[1]))∧(i451[0] →* i451[1])∧(i453[0] > 0 && i451[0] + 1 > 0 →* TRUE)∧(i183[0] →* i183[1]))


(1) -> (0), if ((i183[1] →* i183[0])∧(i451[1] + 1 →* i451[0])∧((o1725[1] →* o1725[0])∧(i453[1] - 1 →* i453[0])))


(1) -> (2), if ((i183[1] →* i183[2])∧((o1725[1] →* java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])))∧(i453[1] - 1 →* i454[2]))∧(i451[1] + 1 →* i451[2]))


(1) -> (4), if (((o1725[1] →* NULL)∧(i453[1] - 1 →* i454[4]))∧(i183[1] →* i183[4])∧(i451[1] + 1 →* i451[4]))


(2) -> (3), if ((i183[2] →* i183[3])∧(i454[2] <= 0 →* TRUE)∧(i451[2] →* i451[3])∧((o1731Field0[2] →* o1731Field0[3])∧(o1731Field1[2] →* o1731Field1[3])∧(i454[2] →* i454[3])))


(3) -> (0), if (((o1731Field0[3] →* o1725[0])∧(o1731Field1[3] →* i453[0]))∧(i451[3] * i183[3] →* i451[0])∧(i183[3] →* i183[0]))


(3) -> (2), if ((i183[3] →* i183[2])∧((o1731Field0[3] →* java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])))∧(o1731Field1[3] →* i454[2]))∧(i451[3] * i183[3] →* i451[2]))


(3) -> (4), if ((i451[3] * i183[3] →* i451[4])∧((o1731Field0[3] →* NULL)∧(o1731Field1[3] →* i454[4]))∧(i183[3] →* i183[4]))


(4) -> (5), if ((i451[4] →* i451[5])∧(i183[4] →* i183[5])∧((i454[4] →* i454[5]))∧(i454[4] <= 0 →* TRUE))


(5) -> (0), if ((i451[5] →* i451[0])∧false∧(i183[5] →* i183[0]))


(5) -> (2), if (false∧(i183[5] →* i183[2])∧(i451[5] →* i451[2]))


(5) -> (4), if ((i183[5] →* i183[4])∧(i451[5] →* i451[4])∧false)



The set Q consists of the following terms:
Load1852(java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load1852(TRUE, java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)
Cond_Load18522(TRUE, java.lang.Object(IntList(NULL, x0)), x1, x2)

(12) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair LOAD1852(java.lang.Object(IntList(o1725, i453)), i183, i451) → COND_LOAD1852(&&(>(i453, 0), >(+(i451, 1), 0)), java.lang.Object(IntList(o1725, i453)), i183, i451) the following chains were created:
  • We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)) which results in the following constraint:

    (1)    (o1725[0]=o1725[1]∧i453[0]=i453[1]∧i451[0]=i451[1]∧&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUE∧i183[0]=i183[1] ⇒ LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])∧(UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥))



    We simplified constraint (1) using rule (IV) which results in the following new constraint:

    (2)    (&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUE ⇒ LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])∧(UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(16)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[0] + [bni_26]i183[0] ≥ 0∧[(-1)bso_27] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(16)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[0] + [bni_26]i183[0] ≥ 0∧[(-1)bso_27] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(16)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[0] + [bni_26]i183[0] ≥ 0∧[(-1)bso_27] ≥ 0)



    We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (6)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[bni_26] ≥ 0∧[bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_27] ≥ 0)







For Pair COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725, i453)), i183, i451) → LOAD1852(java.lang.Object(IntList(o1725, -(i453, 1))), i183, +(i451, 1)) the following chains were created:
  • We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)), LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) which results in the following constraint:

    (7)    (o1725[0]=o1725[1]∧i453[0]=i453[1]∧i451[0]=i451[1]∧&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUE∧i183[0]=i183[1]∧i183[1]=i183[0]1∧+(i451[1], 1)=i451[0]1∧o1725[1]=o1725[0]1∧-(i453[1], 1)=i453[0]1 ⇒ COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))



    We simplified constraint (7) using rules (III), (IV) which results in the following new constraint:

    (8)    (&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUE ⇒ COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥LOAD1852(java.lang.Object(IntList(o1725[0], -(i453[0], 1))), i183[0], +(i451[0], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))



    We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (9)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)



    We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (10)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)



    We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (11)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)



    We simplified constraint (11) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (12)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_28] ≥ 0∧[bni_28] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_28 + (-1)Bound*bni_28] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_29] ≥ 0)



  • We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)), LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) which results in the following constraint:

    (13)    (o1725[0]=o1725[1]∧i453[0]=i453[1]∧i451[0]=i451[1]∧&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUE∧i183[0]=i183[1]∧i183[1]=i183[2]∧o1725[1]=java.lang.Object(IntList(o1731Field0[2], o1731Field1[2]))∧-(i453[1], 1)=i454[2]∧+(i451[1], 1)=i451[2] ⇒ COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))



    We simplified constraint (13) using rules (III), (IV) which results in the following new constraint:

    (14)    (&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUE ⇒ COND_LOAD1852(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i453[0])), i183[0], i451[0])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i453[0])), i183[0], i451[0])≥LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), -(i453[0], 1))), i183[0], +(i451[0], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))



    We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (15)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)



    We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (16)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)



    We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (17)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)



    We simplified constraint (17) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (18)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_28] ≥ 0∧[bni_28] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_28 + (-1)Bound*bni_28] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_29] ≥ 0)



  • We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)), LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) which results in the following constraint:

    (19)    (o1725[0]=o1725[1]∧i453[0]=i453[1]∧i451[0]=i451[1]∧&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUE∧i183[0]=i183[1]∧o1725[1]=NULL∧-(i453[1], 1)=i454[4]∧i183[1]=i183[4]∧+(i451[1], 1)=i451[4] ⇒ COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))



    We simplified constraint (19) using rules (III), (IV) which results in the following new constraint:

    (20)    (&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUE ⇒ COND_LOAD1852(TRUE, java.lang.Object(IntList(NULL, i453[0])), i183[0], i451[0])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(NULL, i453[0])), i183[0], i451[0])≥LOAD1852(java.lang.Object(IntList(NULL, -(i453[0], 1))), i183[0], +(i451[0], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))



    We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (21)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)



    We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (22)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)



    We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (23)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)



    We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (24)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_28] ≥ 0∧[bni_28] ≥ 0∧0 ≥ 0∧[(16)bni_28 + (-1)Bound*bni_28] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_29] ≥ 0)







For Pair LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) → COND_LOAD18521(<=(i454, 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) the following chains were created:
  • We consider the chain LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]), COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3])) which results in the following constraint:

    (25)    (i183[2]=i183[3]∧<=(i454[2], 0)=TRUE∧i451[2]=i451[3]∧o1731Field0[2]=o1731Field0[3]∧o1731Field1[2]=o1731Field1[3]∧i454[2]=i454[3] ⇒ LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥NonInfC∧LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])∧(UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥))



    We simplified constraint (25) using rule (IV) which results in the following new constraint:

    (26)    (<=(i454[2], 0)=TRUE ⇒ LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥NonInfC∧LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])∧(UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥))



    We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (27)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[(16)bni_30 + (-1)Bound*bni_30] + [bni_30]i451[2] + [bni_30]i183[2] ≥ 0∧[(-1)bso_31] ≥ 0)



    We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (28)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[(16)bni_30 + (-1)Bound*bni_30] + [bni_30]i451[2] + [bni_30]i183[2] ≥ 0∧[(-1)bso_31] ≥ 0)



    We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (29)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[(16)bni_30 + (-1)Bound*bni_30] + [bni_30]i451[2] + [bni_30]i183[2] ≥ 0∧[(-1)bso_31] ≥ 0)



    We simplified constraint (29) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (30)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[bni_30] ≥ 0∧[bni_30] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_30 + (-1)Bound*bni_30] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_31] ≥ 0)







For Pair COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) → LOAD1852(java.lang.Object(IntList(o1731Field0, o1731Field1)), i183, *(i451, i183)) the following chains were created:
  • We consider the chain LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]), COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3])), LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) which results in the following constraint:

    (31)    (i183[2]=i183[3]∧<=(i454[2], 0)=TRUE∧i451[2]=i451[3]∧o1731Field0[2]=o1731Field0[3]∧o1731Field1[2]=o1731Field1[3]∧i454[2]=i454[3]∧o1731Field0[3]=o1725[0]∧o1731Field1[3]=i453[0]∧*(i451[3], i183[3])=i451[0]∧i183[3]=i183[0] ⇒ COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))



    We simplified constraint (31) using rules (III), (IV) which results in the following new constraint:

    (32)    (<=(i454[2], 0)=TRUE ⇒ COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥LOAD1852(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i183[2], *(i451[2], i183[2]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))



    We simplified constraint (32) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (33)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)



    We simplified constraint (33) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (34)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)



    We simplified constraint (34) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (35)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)



    We simplified constraint (35) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (36)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_32] ≥ 0∧[bni_32] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_32 + (-1)Bound*bni_32] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_33] ≥ 0)



  • We consider the chain LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]), COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3])), LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) which results in the following constraint:

    (37)    (i183[2]=i183[3]∧<=(i454[2], 0)=TRUE∧i451[2]=i451[3]∧o1731Field0[2]=o1731Field0[3]∧o1731Field1[2]=o1731Field1[3]∧i454[2]=i454[3]∧i183[3]=i183[2]1∧o1731Field0[3]=java.lang.Object(IntList(o1731Field0[2]1, o1731Field1[2]1))∧o1731Field1[3]=i454[2]1∧*(i451[3], i183[3])=i451[2]1 ⇒ COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))



    We simplified constraint (37) using rules (III), (IV) which results in the following new constraint:

    (38)    (<=(i454[2], 0)=TRUE ⇒ COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2]1, o1731Field1[2]1)), o1731Field1[2])), i454[2])), i183[2], i451[2])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2]1, o1731Field1[2]1)), o1731Field1[2])), i454[2])), i183[2], i451[2])≥LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2]1, o1731Field1[2]1)), o1731Field1[2])), i183[2], *(i451[2], i183[2]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))



    We simplified constraint (38) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (39)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)



    We simplified constraint (39) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (40)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)



    We simplified constraint (40) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (41)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)



    We simplified constraint (41) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (42)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_32] ≥ 0∧[bni_32] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_32 + (-1)Bound*bni_32] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_33] ≥ 0)



  • We consider the chain LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]), COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3])), LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) which results in the following constraint:

    (43)    (i183[2]=i183[3]∧<=(i454[2], 0)=TRUE∧i451[2]=i451[3]∧o1731Field0[2]=o1731Field0[3]∧o1731Field1[2]=o1731Field1[3]∧i454[2]=i454[3]∧*(i451[3], i183[3])=i451[4]∧o1731Field0[3]=NULL∧o1731Field1[3]=i454[4]∧i183[3]=i183[4] ⇒ COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))



    We simplified constraint (43) using rules (III), (IV) which results in the following new constraint:

    (44)    (<=(i454[2], 0)=TRUE ⇒ COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(NULL, o1731Field1[2])), i454[2])), i183[2], i451[2])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(NULL, o1731Field1[2])), i454[2])), i183[2], i451[2])≥LOAD1852(java.lang.Object(IntList(NULL, o1731Field1[2])), i183[2], *(i451[2], i183[2]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))



    We simplified constraint (44) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (45)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)



    We simplified constraint (45) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (46)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)



    We simplified constraint (46) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (47)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)



    We simplified constraint (47) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (48)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_32] ≥ 0∧[bni_32] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_32 + (-1)Bound*bni_32] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_33] ≥ 0)







For Pair LOAD1852(java.lang.Object(IntList(NULL, i454)), i183, i451) → COND_LOAD18522(<=(i454, 0), java.lang.Object(IntList(NULL, i454)), i183, i451) the following chains were created:
  • We consider the chain LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]), COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5]) → LOAD1852(NULL, i183[5], i451[5]) which results in the following constraint:

    (49)    (i451[4]=i451[5]∧i183[4]=i183[5]∧i454[4]=i454[5]∧<=(i454[4], 0)=TRUE ⇒ LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])≥NonInfC∧LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])≥COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])∧(UIncreasing(COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])), ≥))



    We simplified constraint (49) using rule (IV) which results in the following new constraint:

    (50)    (<=(i454[4], 0)=TRUE ⇒ LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])≥NonInfC∧LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])≥COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])∧(UIncreasing(COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])), ≥))



    We simplified constraint (50) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (51)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])), ≥)∧[(16)bni_34 + (-1)Bound*bni_34] + [bni_34]i451[4] + [bni_34]i183[4] ≥ 0∧[15 + (-1)bso_35] ≥ 0)



    We simplified constraint (51) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (52)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])), ≥)∧[(16)bni_34 + (-1)Bound*bni_34] + [bni_34]i451[4] + [bni_34]i183[4] ≥ 0∧[15 + (-1)bso_35] ≥ 0)



    We simplified constraint (52) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (53)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])), ≥)∧[(16)bni_34 + (-1)Bound*bni_34] + [bni_34]i451[4] + [bni_34]i183[4] ≥ 0∧[15 + (-1)bso_35] ≥ 0)



    We simplified constraint (53) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (54)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])), ≥)∧[bni_34] ≥ 0∧[bni_34] ≥ 0∧0 ≥ 0∧[(16)bni_34 + (-1)Bound*bni_34] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[15 + (-1)bso_35] ≥ 0)







For Pair COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454)), i183, i451) → LOAD1852(NULL, i183, i451) the following chains were created:
  • We consider the chain LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]), COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5]) → LOAD1852(NULL, i183[5], i451[5]), LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) which results in the following constraint:

    (55)    (COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5])≥NonInfC∧COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5])≥LOAD1852(NULL, i183[5], i451[5])∧(UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥))



    We simplified constraint (55) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (56)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)



    We simplified constraint (56) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (57)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)



    We simplified constraint (57) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (58)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)



    We simplified constraint (58) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (59)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_37] ≥ 0)



  • We consider the chain LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]), COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5]) → LOAD1852(NULL, i183[5], i451[5]), LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) which results in the following constraint:

    (60)    (COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5])≥NonInfC∧COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5])≥LOAD1852(NULL, i183[5], i451[5])∧(UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥))



    We simplified constraint (60) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (61)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)



    We simplified constraint (61) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (62)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)



    We simplified constraint (62) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (63)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)



    We simplified constraint (63) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (64)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_37] ≥ 0)



  • We consider the chain LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]), COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5]) → LOAD1852(NULL, i183[5], i451[5]), LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) which results in the following constraint:

    (65)    (COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5])≥NonInfC∧COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5])≥LOAD1852(NULL, i183[5], i451[5])∧(UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥))



    We simplified constraint (65) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (66)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)



    We simplified constraint (66) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (67)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)



    We simplified constraint (67) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (68)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)



    We simplified constraint (68) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (69)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_37] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • LOAD1852(java.lang.Object(IntList(o1725, i453)), i183, i451) → COND_LOAD1852(&&(>(i453, 0), >(+(i451, 1), 0)), java.lang.Object(IntList(o1725, i453)), i183, i451)
    • (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[bni_26] ≥ 0∧[bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_27] ≥ 0)

  • COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725, i453)), i183, i451) → LOAD1852(java.lang.Object(IntList(o1725, -(i453, 1))), i183, +(i451, 1))
    • (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_28] ≥ 0∧[bni_28] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_28 + (-1)Bound*bni_28] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_29] ≥ 0)
    • (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_28] ≥ 0∧[bni_28] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_28 + (-1)Bound*bni_28] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_29] ≥ 0)
    • (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_28] ≥ 0∧[bni_28] ≥ 0∧0 ≥ 0∧[(16)bni_28 + (-1)Bound*bni_28] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_29] ≥ 0)

  • LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) → COND_LOAD18521(<=(i454, 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451)
    • (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[bni_30] ≥ 0∧[bni_30] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_30 + (-1)Bound*bni_30] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_31] ≥ 0)

  • COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) → LOAD1852(java.lang.Object(IntList(o1731Field0, o1731Field1)), i183, *(i451, i183))
    • (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_32] ≥ 0∧[bni_32] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_32 + (-1)Bound*bni_32] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_33] ≥ 0)
    • (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_32] ≥ 0∧[bni_32] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_32 + (-1)Bound*bni_32] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_33] ≥ 0)
    • (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_32] ≥ 0∧[bni_32] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_32 + (-1)Bound*bni_32] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_33] ≥ 0)

  • LOAD1852(java.lang.Object(IntList(NULL, i454)), i183, i451) → COND_LOAD18522(<=(i454, 0), java.lang.Object(IntList(NULL, i454)), i183, i451)
    • (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])), ≥)∧[bni_34] ≥ 0∧[bni_34] ≥ 0∧0 ≥ 0∧[(16)bni_34 + (-1)Bound*bni_34] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[15 + (-1)bso_35] ≥ 0)

  • COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454)), i183, i451) → LOAD1852(NULL, i183, i451)
    • ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_37] ≥ 0)
    • ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_37] ≥ 0)
    • ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_37] ≥ 0)




The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers with natural coefficients for all symbols [NONINF][POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(LOAD1852(x1, x2, x3)) = x3 + x2 + [2]x1   
POL(java.lang.Object(x1)) = [2] + [2]x1   
POL(IntList(x1, x2)) = [3]   
POL(COND_LOAD1852(x1, x2, x3, x4)) = x4 + x3 + [2]x2 + [3]x1   
POL(&&(x1, x2)) = 0   
POL(>(x1, x2)) = 0   
POL(0) = 0   
POL(+(x1, x2)) = 0   
POL(1) = 0   
POL(-(x1, x2)) = 0   
POL(COND_LOAD18521(x1, x2, x3, x4)) = x4 + x3 + [2]x2   
POL(<=(x1, x2)) = 0   
POL(*(x1, x2)) = 0   
POL(NULL) = 0   
POL(COND_LOAD18522(x1, x2, x3, x4)) = [1] + x4 + x3   

The following pairs are in P>:

LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])
COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5]) → LOAD1852(NULL, i183[5], i451[5])

The following pairs are in Pbound:

LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))
LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))
LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])

The following pairs are in P≥:

LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))
LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))

At least the following rules have been oriented under context sensitive arithmetic replacement:

&&(TRUE, TRUE)1 → TRUE1
&&(TRUE, FALSE)1 → FALSE1
&&(FALSE, TRUE)1 → FALSE1
&&(FALSE, FALSE)1 → FALSE1

(13) Complex Obligation (AND)

(14) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(i453[0] > 0 && i451[0] + 1 > 0, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
(1): COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], i453[1] - 1)), i183[1], i451[1] + 1)
(2): LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(i454[2] <= 0, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
(3): COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], i451[3] * i183[3])

(1) -> (0), if ((i183[1] →* i183[0])∧(i451[1] + 1 →* i451[0])∧((o1725[1] →* o1725[0])∧(i453[1] - 1 →* i453[0])))


(3) -> (0), if (((o1731Field0[3] →* o1725[0])∧(o1731Field1[3] →* i453[0]))∧(i451[3] * i183[3] →* i451[0])∧(i183[3] →* i183[0]))


(0) -> (1), if (((o1725[0] →* o1725[1])∧(i453[0] →* i453[1]))∧(i451[0] →* i451[1])∧(i453[0] > 0 && i451[0] + 1 > 0 →* TRUE)∧(i183[0] →* i183[1]))


(1) -> (2), if ((i183[1] →* i183[2])∧((o1725[1] →* java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])))∧(i453[1] - 1 →* i454[2]))∧(i451[1] + 1 →* i451[2]))


(3) -> (2), if ((i183[3] →* i183[2])∧((o1731Field0[3] →* java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])))∧(o1731Field1[3] →* i454[2]))∧(i451[3] * i183[3] →* i451[2]))


(2) -> (3), if ((i183[2] →* i183[3])∧(i454[2] <= 0 →* TRUE)∧(i451[2] →* i451[3])∧((o1731Field0[2] →* o1731Field0[3])∧(o1731Field1[2] →* o1731Field1[3])∧(i454[2] →* i454[3])))



The set Q consists of the following terms:
Load1852(java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load1852(TRUE, java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)
Cond_Load18522(TRUE, java.lang.Object(IntList(NULL, x0)), x1, x2)

(15) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) the following chains were created:
  • We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)) which results in the following constraint:

    (1)    (o1725[0]=o1725[1]∧i453[0]=i453[1]∧i451[0]=i451[1]∧&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUE∧i183[0]=i183[1] ⇒ LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])∧(UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥))



    We simplified constraint (1) using rule (IV) which results in the following new constraint:

    (2)    (&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUE ⇒ LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])∧(UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(2)bni_20 + (-1)Bound*bni_20] + [(2)bni_20]i451[0] + [(2)bni_20]i183[0] + [(4)bni_20]o1725[0] ≥ 0∧[(-1)bso_21] + i451[0] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(2)bni_20 + (-1)Bound*bni_20] + [(2)bni_20]i451[0] + [(2)bni_20]i183[0] + [(4)bni_20]o1725[0] ≥ 0∧[(-1)bso_21] + i451[0] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(2)bni_20 + (-1)Bound*bni_20] + [(2)bni_20]i451[0] + [(2)bni_20]i183[0] + [(4)bni_20]o1725[0] ≥ 0∧[(-1)bso_21] + i451[0] ≥ 0)



    We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (6)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(2)bni_20] ≥ 0∧[(2)bni_20] ≥ 0∧0 ≥ 0∧[(4)bni_20] ≥ 0∧[(2)bni_20 + (-1)Bound*bni_20] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_21] ≥ 0)







For Pair COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)) the following chains were created:
  • We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)), LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) which results in the following constraint:

    (7)    (o1725[0]=o1725[1]∧i453[0]=i453[1]∧i451[0]=i451[1]∧&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUE∧i183[0]=i183[1]∧i183[1]=i183[0]1∧+(i451[1], 1)=i451[0]1∧o1725[1]=o1725[0]1∧-(i453[1], 1)=i453[0]1 ⇒ COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))



    We simplified constraint (7) using rules (III), (IV) which results in the following new constraint:

    (8)    (&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUE ⇒ COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥LOAD1852(java.lang.Object(IntList(o1725[0], -(i453[0], 1))), i183[0], +(i451[0], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))



    We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (9)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(2)bni_22 + (-1)Bound*bni_22] + [bni_22]i451[0] + [(2)bni_22]i183[0] + [(4)bni_22]o1725[0] ≥ 0∧[(-1)bso_23] + i451[0] ≥ 0)



    We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (10)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(2)bni_22 + (-1)Bound*bni_22] + [bni_22]i451[0] + [(2)bni_22]i183[0] + [(4)bni_22]o1725[0] ≥ 0∧[(-1)bso_23] + i451[0] ≥ 0)



    We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (11)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(2)bni_22 + (-1)Bound*bni_22] + [bni_22]i451[0] + [(2)bni_22]i183[0] + [(4)bni_22]o1725[0] ≥ 0∧[(-1)bso_23] + i451[0] ≥ 0)



    We simplified constraint (11) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (12)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_22] ≥ 0∧[(2)bni_22] ≥ 0∧0 ≥ 0∧[(4)bni_22] ≥ 0∧[(2)bni_22 + (-1)Bound*bni_22] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_23] ≥ 0)



  • We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)), LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) which results in the following constraint:

    (13)    (o1725[0]=o1725[1]∧i453[0]=i453[1]∧i451[0]=i451[1]∧&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUE∧i183[0]=i183[1]∧i183[1]=i183[2]∧o1725[1]=java.lang.Object(IntList(o1731Field0[2], o1731Field1[2]))∧-(i453[1], 1)=i454[2]∧+(i451[1], 1)=i451[2] ⇒ COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))



    We simplified constraint (13) using rules (III), (IV) which results in the following new constraint:

    (14)    (&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUE ⇒ COND_LOAD1852(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i453[0])), i183[0], i451[0])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i453[0])), i183[0], i451[0])≥LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), -(i453[0], 1))), i183[0], +(i451[0], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))



    We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (15)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(6)bni_22 + (-1)Bound*bni_22] + [bni_22]i451[0] + [(2)bni_22]i183[0] + [(8)bni_22]o1731Field0[2] ≥ 0∧[(-1)bso_23] + i451[0] ≥ 0)



    We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (16)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(6)bni_22 + (-1)Bound*bni_22] + [bni_22]i451[0] + [(2)bni_22]i183[0] + [(8)bni_22]o1731Field0[2] ≥ 0∧[(-1)bso_23] + i451[0] ≥ 0)



    We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (17)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(6)bni_22 + (-1)Bound*bni_22] + [bni_22]i451[0] + [(2)bni_22]i183[0] + [(8)bni_22]o1731Field0[2] ≥ 0∧[(-1)bso_23] + i451[0] ≥ 0)



    We simplified constraint (17) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (18)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_22] ≥ 0∧[(2)bni_22] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(8)bni_22] ≥ 0∧[(6)bni_22 + (-1)Bound*bni_22] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_23] ≥ 0)







For Pair LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) the following chains were created:
  • We consider the chain LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]), COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3])) which results in the following constraint:

    (19)    (i183[2]=i183[3]∧<=(i454[2], 0)=TRUE∧i451[2]=i451[3]∧o1731Field0[2]=o1731Field0[3]∧o1731Field1[2]=o1731Field1[3]∧i454[2]=i454[3] ⇒ LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥NonInfC∧LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])∧(UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥))



    We simplified constraint (19) using rule (IV) which results in the following new constraint:

    (20)    (<=(i454[2], 0)=TRUE ⇒ LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥NonInfC∧LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])∧(UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥))



    We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (21)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[(6)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i451[2] + [(2)bni_24]i183[2] + [(8)bni_24]o1731Field0[2] ≥ 0∧[3 + (-1)bso_25] + i451[2] + [4]o1731Field0[2] ≥ 0)



    We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (22)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[(6)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i451[2] + [(2)bni_24]i183[2] + [(8)bni_24]o1731Field0[2] ≥ 0∧[3 + (-1)bso_25] + i451[2] + [4]o1731Field0[2] ≥ 0)



    We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (23)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[(6)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i451[2] + [(2)bni_24]i183[2] + [(8)bni_24]o1731Field0[2] ≥ 0∧[3 + (-1)bso_25] + i451[2] + [4]o1731Field0[2] ≥ 0)



    We simplified constraint (23) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:

    (24)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[(2)bni_24] ≥ 0∧[(2)bni_24] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(8)bni_24] ≥ 0∧[(6)bni_24 + (-1)Bound*bni_24] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[3 + (-1)bso_25] ≥ 0∧[1] ≥ 0)







For Pair COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3])) the following chains were created:
  • We consider the chain LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]), COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3])), LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) which results in the following constraint:

    (25)    (i183[2]=i183[3]∧<=(i454[2], 0)=TRUE∧i451[2]=i451[3]∧o1731Field0[2]=o1731Field0[3]∧o1731Field1[2]=o1731Field1[3]∧i454[2]=i454[3]∧o1731Field0[3]=o1725[0]∧o1731Field1[3]=i453[0]∧*(i451[3], i183[3])=i451[0]∧i183[3]=i183[0] ⇒ COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))



    We simplified constraint (25) using rules (III), (IV) which results in the following new constraint:

    (26)    (<=(i454[2], 0)=TRUE ⇒ COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥LOAD1852(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i183[2], *(i451[2], i183[2]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))



    We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (27)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(3)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[2] + [(2)bni_26]i183[2] + [(4)bni_26]o1731Field0[2] ≥ 0∧[1 + (-1)bso_27] + i451[2] ≥ 0)



    We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (28)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(3)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[2] + [(2)bni_26]i183[2] + [(4)bni_26]o1731Field0[2] ≥ 0∧[1 + (-1)bso_27] + i451[2] ≥ 0)



    We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (29)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(3)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[2] + [(2)bni_26]i183[2] + [(4)bni_26]o1731Field0[2] ≥ 0∧[1 + (-1)bso_27] + i451[2] ≥ 0)



    We simplified constraint (29) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (30)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_26] ≥ 0∧[(2)bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(4)bni_26] ≥ 0∧[(3)bni_26 + (-1)Bound*bni_26] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_27] ≥ 0)



  • We consider the chain LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]), COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3])), LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) which results in the following constraint:

    (31)    (i183[2]=i183[3]∧<=(i454[2], 0)=TRUE∧i451[2]=i451[3]∧o1731Field0[2]=o1731Field0[3]∧o1731Field1[2]=o1731Field1[3]∧i454[2]=i454[3]∧i183[3]=i183[2]1∧o1731Field0[3]=java.lang.Object(IntList(o1731Field0[2]1, o1731Field1[2]1))∧o1731Field1[3]=i454[2]1∧*(i451[3], i183[3])=i451[2]1 ⇒ COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))



    We simplified constraint (31) using rules (III), (IV) which results in the following new constraint:

    (32)    (<=(i454[2], 0)=TRUE ⇒ COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2]1, o1731Field1[2]1)), o1731Field1[2])), i454[2])), i183[2], i451[2])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2]1, o1731Field1[2]1)), o1731Field1[2])), i454[2])), i183[2], i451[2])≥LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2]1, o1731Field1[2]1)), o1731Field1[2])), i183[2], *(i451[2], i183[2]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))



    We simplified constraint (32) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (33)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(7)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[2] + [(2)bni_26]i183[2] + [(8)bni_26]o1731Field0[2]1 ≥ 0∧[1 + (-1)bso_27] + i451[2] ≥ 0)



    We simplified constraint (33) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (34)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(7)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[2] + [(2)bni_26]i183[2] + [(8)bni_26]o1731Field0[2]1 ≥ 0∧[1 + (-1)bso_27] + i451[2] ≥ 0)



    We simplified constraint (34) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (35)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(7)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[2] + [(2)bni_26]i183[2] + [(8)bni_26]o1731Field0[2]1 ≥ 0∧[1 + (-1)bso_27] + i451[2] ≥ 0)



    We simplified constraint (35) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (36)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_26] ≥ 0∧[(2)bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(8)bni_26] ≥ 0∧[(7)bni_26 + (-1)Bound*bni_26] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_27] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
    • (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(2)bni_20] ≥ 0∧[(2)bni_20] ≥ 0∧0 ≥ 0∧[(4)bni_20] ≥ 0∧[(2)bni_20 + (-1)Bound*bni_20] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_21] ≥ 0)

  • COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))
    • (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_22] ≥ 0∧[(2)bni_22] ≥ 0∧0 ≥ 0∧[(4)bni_22] ≥ 0∧[(2)bni_22 + (-1)Bound*bni_22] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_23] ≥ 0)
    • (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_22] ≥ 0∧[(2)bni_22] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(8)bni_22] ≥ 0∧[(6)bni_22 + (-1)Bound*bni_22] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_23] ≥ 0)

  • LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
    • (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[(2)bni_24] ≥ 0∧[(2)bni_24] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(8)bni_24] ≥ 0∧[(6)bni_24 + (-1)Bound*bni_24] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[3 + (-1)bso_25] ≥ 0∧[1] ≥ 0)

  • COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))
    • (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_26] ≥ 0∧[(2)bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(4)bni_26] ≥ 0∧[(3)bni_26 + (-1)Bound*bni_26] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_27] ≥ 0)
    • (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_26] ≥ 0∧[(2)bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(8)bni_26] ≥ 0∧[(7)bni_26 + (-1)Bound*bni_26] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_27] ≥ 0)




The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers with natural coefficients for all symbols [NONINF][POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(LOAD1852(x1, x2, x3)) = [2]x3 + [2]x2 + [2]x1   
POL(java.lang.Object(x1)) = x1   
POL(IntList(x1, x2)) = [1] + [2]x1   
POL(COND_LOAD1852(x1, x2, x3, x4)) = x4 + [2]x3 + [2]x2 + [3]x1   
POL(&&(x1, x2)) = 0   
POL(>(x1, x2)) = 0   
POL(0) = 0   
POL(+(x1, x2)) = 0   
POL(1) = 0   
POL(-(x1, x2)) = 0   
POL(COND_LOAD18521(x1, x2, x3, x4)) = x4 + [2]x3 + x2   
POL(<=(x1, x2)) = 0   
POL(*(x1, x2)) = 0   

The following pairs are in P>:

LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))

The following pairs are in Pbound:

LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))
LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))

The following pairs are in P≥:

LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))

At least the following rules have been oriented under context sensitive arithmetic replacement:

&&(TRUE, TRUE)1 ↔ TRUE1
&&(TRUE, FALSE)1 ↔ FALSE1
&&(FALSE, TRUE)1 ↔ FALSE1
&&(FALSE, FALSE)1 ↔ FALSE1

(16) Complex Obligation (AND)

(17) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(i453[0] > 0 && i451[0] + 1 > 0, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
(1): COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], i453[1] - 1)), i183[1], i451[1] + 1)

(1) -> (0), if ((i183[1] →* i183[0])∧(i451[1] + 1 →* i451[0])∧((o1725[1] →* o1725[0])∧(i453[1] - 1 →* i453[0])))


(0) -> (1), if (((o1725[0] →* o1725[1])∧(i453[0] →* i453[1]))∧(i451[0] →* i451[1])∧(i453[0] > 0 && i451[0] + 1 > 0 →* TRUE)∧(i183[0] →* i183[1]))



The set Q consists of the following terms:
Load1852(java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load1852(TRUE, java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)
Cond_Load18522(TRUE, java.lang.Object(IntList(NULL, x0)), x1, x2)

(18) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) the following chains were created:
  • We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)) which results in the following constraint:

    (1)    (o1725[0]=o1725[1]∧i453[0]=i453[1]∧i451[0]=i451[1]∧&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUE∧i183[0]=i183[1] ⇒ LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])∧(UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥))



    We simplified constraint (1) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (2)    (>(i453[0], 0)=TRUE∧>(+(i451[0], 1), 0)=TRUE ⇒ LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])∧(UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (i453[0] + [-1] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(-1)Bound*bni_19] + [bni_19]i453[0] ≥ 0∧[(-1)bso_20] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (i453[0] + [-1] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(-1)Bound*bni_19] + [bni_19]i453[0] ≥ 0∧[(-1)bso_20] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (i453[0] + [-1] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(-1)Bound*bni_19] + [bni_19]i453[0] ≥ 0∧[(-1)bso_20] ≥ 0)



    We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (6)    (i453[0] + [-1] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_19] + [bni_19]i453[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_20] ≥ 0)



    We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (7)    (i453[0] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_19 + bni_19] + [bni_19]i453[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_20] ≥ 0)







For Pair COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)) the following chains were created:
  • We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)), LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) which results in the following constraint:

    (8)    (o1725[0]=o1725[1]∧i453[0]=i453[1]∧i451[0]=i451[1]∧&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUE∧i183[0]=i183[1]∧i183[1]=i183[0]1∧+(i451[1], 1)=i451[0]1∧o1725[1]=o1725[0]1∧-(i453[1], 1)=i453[0]1 ⇒ COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))



    We simplified constraint (8) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (9)    (>(i453[0], 0)=TRUE∧>(+(i451[0], 1), 0)=TRUE ⇒ COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥LOAD1852(java.lang.Object(IntList(o1725[0], -(i453[0], 1))), i183[0], +(i451[0], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))



    We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (10)    (i453[0] + [-1] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(-1)Bound*bni_21] + [bni_21]i453[0] ≥ 0∧[1 + (-1)bso_22] ≥ 0)



    We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (11)    (i453[0] + [-1] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(-1)Bound*bni_21] + [bni_21]i453[0] ≥ 0∧[1 + (-1)bso_22] ≥ 0)



    We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (12)    (i453[0] + [-1] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(-1)Bound*bni_21] + [bni_21]i453[0] ≥ 0∧[1 + (-1)bso_22] ≥ 0)



    We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (13)    (i453[0] + [-1] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_21] + [bni_21]i453[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)



    We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (14)    (i453[0] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_21 + bni_21] + [bni_21]i453[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
    • (i453[0] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_19 + bni_19] + [bni_19]i453[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_20] ≥ 0)

  • COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))
    • (i453[0] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_21 + bni_21] + [bni_21]i453[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)




The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = [1]   
POL(LOAD1852(x1, x2, x3)) = [-1] + [-1]x1   
POL(java.lang.Object(x1)) = x1   
POL(IntList(x1, x2)) = [-1] + [-1]x2   
POL(COND_LOAD1852(x1, x2, x3, x4)) = [-1] + [-1]x2 + [-1]x1   
POL(&&(x1, x2)) = 0   
POL(>(x1, x2)) = [-1]   
POL(0) = 0   
POL(+(x1, x2)) = x1 + x2   
POL(1) = [1]   
POL(-(x1, x2)) = x1 + [-1]x2   

The following pairs are in P>:

COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))

The following pairs are in Pbound:

LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))

The following pairs are in P≥:

LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])

At least the following rules have been oriented under context sensitive arithmetic replacement:

TRUE1 → &&(TRUE, TRUE)1
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1

(19) Complex Obligation (AND)

(20) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(i453[0] > 0 && i451[0] + 1 > 0, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])


The set Q consists of the following terms:
Load1852(java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load1852(TRUE, java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)
Cond_Load18522(TRUE, java.lang.Object(IntList(NULL, x0)), x1, x2)

(21) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(22) TRUE

(23) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:
none


R is empty.

The integer pair graph is empty.

The set Q consists of the following terms:
Load1852(java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load1852(TRUE, java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)
Cond_Load18522(TRUE, java.lang.Object(IntList(NULL, x0)), x1, x2)

(24) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

(25) TRUE

(26) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:
none


R is empty.

The integer pair graph is empty.

The set Q consists of the following terms:
Load1852(java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load1852(TRUE, java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)
Cond_Load18522(TRUE, java.lang.Object(IntList(NULL, x0)), x1, x2)

(27) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs.

(28) TRUE

(29) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:
none


R is empty.

The integer pair graph contains the following rules and edges:
(5): COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5]) → LOAD1852(NULL, i183[5], i451[5])


The set Q consists of the following terms:
Load1852(java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load1852(TRUE, java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)
Cond_Load18522(TRUE, java.lang.Object(IntList(NULL, x0)), x1, x2)

(30) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(31) TRUE

(32) Obligation:

ITRS problem:

The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load1102(java.lang.Object(ARRAY(i3, a1201data)), i96, i98) → Load1102ARR1(java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572)))
Load1102ARR1(java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) → Cond_Load1102ARR1(i96 > 0 && i96 < i3 && i98 > 0 && i96 + 1 > 0, java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572)))
Cond_Load1102ARR1(TRUE, java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) → Load1102(java.lang.Object(ARRAY(i3, a1201data)), i96 + 1, i98 + -1)
The set Q consists of the following terms:
Load1102(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load1102ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1102ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

(33) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(34) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


The ITRS R consists of the following rules:
Load1102(java.lang.Object(ARRAY(i3, a1201data)), i96, i98) → Load1102ARR1(java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572)))
Load1102ARR1(java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) → Cond_Load1102ARR1(i96 > 0 && i96 < i3 && i98 > 0 && i96 + 1 > 0, java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572)))
Cond_Load1102ARR1(TRUE, java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) → Load1102(java.lang.Object(ARRAY(i3, a1201data)), i96 + 1, i98 + -1)

The integer pair graph contains the following rules and edges:
(0): LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0]) → LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))
(1): LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1]))) → COND_LOAD1102ARR1(i96[1] > 0 && i96[1] < i3[1] && i98[1] > 0 && i96[1] + 1 > 0, java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))
(2): COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2]))) → LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2] + 1, i98[2] + -1)

(0) -> (1), if ((i98[0] →* i98[1])∧(java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])) →* java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))∧(java.lang.Object(ARRAY(i3[0], a1201data[0])) →* java.lang.Object(ARRAY(i3[1], a1201data[1])))∧(i96[0] →* i96[1]))


(1) -> (2), if ((i96[1] →* i96[2])∧(java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])) →* java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2])))∧(i98[1] →* i98[2])∧(java.lang.Object(ARRAY(i3[1], a1201data[1])) →* java.lang.Object(ARRAY(i3[2], a1201data[2])))∧(i96[1] > 0 && i96[1] < i3[1] && i98[1] > 0 && i96[1] + 1 > 0 →* TRUE))


(2) -> (0), if ((i98[2] + -1 →* i98[0])∧(java.lang.Object(ARRAY(i3[2], a1201data[2])) →* java.lang.Object(ARRAY(i3[0], a1201data[0])))∧(i96[2] + 1 →* i96[0]))



The set Q consists of the following terms:
Load1102(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load1102ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1102ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

(35) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(36) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0]) → LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))
(1): LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1]))) → COND_LOAD1102ARR1(i96[1] > 0 && i96[1] < i3[1] && i98[1] > 0 && i96[1] + 1 > 0, java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))
(2): COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2]))) → LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2] + 1, i98[2] + -1)

(0) -> (1), if ((i98[0] →* i98[1])∧(java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])) →* java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))∧(java.lang.Object(ARRAY(i3[0], a1201data[0])) →* java.lang.Object(ARRAY(i3[1], a1201data[1])))∧(i96[0] →* i96[1]))


(1) -> (2), if ((i96[1] →* i96[2])∧(java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])) →* java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2])))∧(i98[1] →* i98[2])∧(java.lang.Object(ARRAY(i3[1], a1201data[1])) →* java.lang.Object(ARRAY(i3[2], a1201data[2])))∧(i96[1] > 0 && i96[1] < i3[1] && i98[1] > 0 && i96[1] + 1 > 0 →* TRUE))


(2) -> (0), if ((i98[2] + -1 →* i98[0])∧(java.lang.Object(ARRAY(i3[2], a1201data[2])) →* java.lang.Object(ARRAY(i3[0], a1201data[0])))∧(i96[2] + 1 →* i96[0]))



The set Q consists of the following terms:
Load1102(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load1102ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1102ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

(37) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

(38) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0]) → LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))
(1): LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1]))) → COND_LOAD1102ARR1(i96[1] > 0 && i96[1] < i3[1] && i98[1] > 0 && i96[1] + 1 > 0, java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))
(2): COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2]))) → LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2] + 1, i98[2] + -1)

(0) -> (1), if ((i98[0] →* i98[1])∧((i175[0] →* i175[1])∧(i174[0] →* i174[1])∧(i176[0] →* i176[1])∧(a1572[0] →* a1572[1]))∧((i3[0] →* i3[1])∧(a1201data[0] →* a1201data[1]))∧(i96[0] →* i96[1]))


(1) -> (2), if ((i96[1] →* i96[2])∧((i175[1] →* i175[2])∧(i174[1] →* i174[2])∧(i176[1] →* i176[2])∧(a1572[1] →* a1572[2]))∧(i98[1] →* i98[2])∧((i3[1] →* i3[2])∧(a1201data[1] →* a1201data[2]))∧(i96[1] > 0 && i96[1] < i3[1] && i98[1] > 0 && i96[1] + 1 > 0 →* TRUE))


(2) -> (0), if ((i98[2] + -1 →* i98[0])∧((i3[2] →* i3[0])∧(a1201data[2] →* a1201data[0]))∧(i96[2] + 1 →* i96[0]))



The set Q consists of the following terms:
Load1102(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load1102ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1102ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

(39) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair LOAD1102(java.lang.Object(ARRAY(i3, a1201data)), i96, i98) → LOAD1102ARR1(java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) the following chains were created:
  • We consider the chain LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0]) → LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0]))) which results in the following constraint:

    (1)    (LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0])≥NonInfC∧LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0])≥LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))∧(UIncreasing(LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))), ≥))



    We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (2)    ((UIncreasing(LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))), ≥)∧[(-1)bso_17] ≥ 0)



    We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (3)    ((UIncreasing(LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))), ≥)∧[(-1)bso_17] ≥ 0)



    We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (4)    ((UIncreasing(LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))), ≥)∧[(-1)bso_17] ≥ 0)



    We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (5)    ((UIncreasing(LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)







For Pair LOAD1102ARR1(java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) → COND_LOAD1102ARR1(&&(&&(&&(>(i96, 0), <(i96, i3)), >(i98, 0)), >(+(i96, 1), 0)), java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) the following chains were created:
  • We consider the chain LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1]))) → COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1]))), COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2]))) → LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1)) which results in the following constraint:

    (6)    (i96[1]=i96[2]∧i175[1]=i175[2]∧i174[1]=i174[2]∧i176[1]=i176[2]∧a1572[1]=a1572[2]∧i98[1]=i98[2]∧i3[1]=i3[2]∧a1201data[1]=a1201data[2]∧&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0))=TRUE ⇒ LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))≥NonInfC∧LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))≥COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))∧(UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥))



    We simplified constraint (6) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (7)    (>(+(i96[1], 1), 0)=TRUE∧>(i98[1], 0)=TRUE∧>(i96[1], 0)=TRUE∧<(i96[1], i3[1])=TRUE ⇒ LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))≥NonInfC∧LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))≥COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))∧(UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥))



    We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (8)    (i96[1] ≥ 0∧i98[1] + [-1] ≥ 0∧i96[1] + [-1] ≥ 0∧i3[1] + [-1] + [-1]i96[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥)∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i98[1] + [(-1)bni_18]i96[1] + [bni_18]i3[1] ≥ 0∧[(-1)bso_19] ≥ 0)



    We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (9)    (i96[1] ≥ 0∧i98[1] + [-1] ≥ 0∧i96[1] + [-1] ≥ 0∧i3[1] + [-1] + [-1]i96[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥)∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i98[1] + [(-1)bni_18]i96[1] + [bni_18]i3[1] ≥ 0∧[(-1)bso_19] ≥ 0)



    We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (10)    (i96[1] ≥ 0∧i98[1] + [-1] ≥ 0∧i96[1] + [-1] ≥ 0∧i3[1] + [-1] + [-1]i96[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥)∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i98[1] + [(-1)bni_18]i96[1] + [bni_18]i3[1] ≥ 0∧[(-1)bso_19] ≥ 0)



    We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (11)    (i96[1] ≥ 0∧i98[1] + [-1] ≥ 0∧i96[1] + [-1] ≥ 0∧i3[1] + [-1] + [-1]i96[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥)∧0 = 0∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i98[1] + [(-1)bni_18]i96[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)



    We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (12)    ([1] + i96[1] ≥ 0∧i98[1] + [-1] ≥ 0∧i96[1] ≥ 0∧i3[1] + [-2] + [-1]i96[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥)∧0 = 0∧[bni_18 + (-1)Bound*bni_18] + [bni_18]i98[1] + [(-1)bni_18]i96[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)



    We simplified constraint (12) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (13)    ([1] + i96[1] ≥ 0∧i98[1] ≥ 0∧i96[1] ≥ 0∧i3[1] + [-2] + [-1]i96[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥)∧0 = 0∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i98[1] + [(-1)bni_18]i96[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)



    We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (14)    ([1] + i96[1] ≥ 0∧i98[1] ≥ 0∧i96[1] ≥ 0∧i3[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥)∧0 = 0∧[(4)bni_18 + (-1)Bound*bni_18] + [bni_18]i98[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)







For Pair COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) → LOAD1102(java.lang.Object(ARRAY(i3, a1201data)), +(i96, 1), +(i98, -1)) the following chains were created:
  • We consider the chain COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2]))) → LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1)) which results in the following constraint:

    (15)    (COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2])))≥NonInfC∧COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2])))≥LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1))∧(UIncreasing(LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1))), ≥))



    We simplified constraint (15) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (16)    ((UIncreasing(LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1))), ≥)∧[2 + (-1)bso_21] ≥ 0)



    We simplified constraint (16) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (17)    ((UIncreasing(LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1))), ≥)∧[2 + (-1)bso_21] ≥ 0)



    We simplified constraint (17) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (18)    ((UIncreasing(LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1))), ≥)∧[2 + (-1)bso_21] ≥ 0)



    We simplified constraint (18) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (19)    ((UIncreasing(LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_21] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • LOAD1102(java.lang.Object(ARRAY(i3, a1201data)), i96, i98) → LOAD1102ARR1(java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572)))
    • ((UIncreasing(LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

  • LOAD1102ARR1(java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) → COND_LOAD1102ARR1(&&(&&(&&(>(i96, 0), <(i96, i3)), >(i98, 0)), >(+(i96, 1), 0)), java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572)))
    • ([1] + i96[1] ≥ 0∧i98[1] ≥ 0∧i96[1] ≥ 0∧i3[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥)∧0 = 0∧[(4)bni_18 + (-1)Bound*bni_18] + [bni_18]i98[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)

  • COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) → LOAD1102(java.lang.Object(ARRAY(i3, a1201data)), +(i96, 1), +(i98, -1))
    • ((UIncreasing(LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_21] ≥ 0)




The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(LOAD1102(x1, x2, x3)) = [1] + x3 + [-1]x2 + [-1]x1   
POL(java.lang.Object(x1)) = x1   
POL(ARRAY(x1, x2)) = [-1] + [-1]x1   
POL(LOAD1102ARR1(x1, x2, x3, x4)) = [1] + x3 + [-1]x2 + [-1]x1   
POL(java.lang.String(x1, x2, x3, x4)) = [-1]   
POL(COND_LOAD1102ARR1(x1, x2, x3, x4, x5)) = [1] + x4 + [-1]x3 + [-1]x2   
POL(&&(x1, x2)) = [-1]   
POL(>(x1, x2)) = [-1]   
POL(0) = 0   
POL(<(x1, x2)) = [-1]   
POL(+(x1, x2)) = x1 + x2   
POL(1) = [1]   
POL(-1) = [-1]   

The following pairs are in P>:

COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2]))) → LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1))

The following pairs are in Pbound:

LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1]))) → COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))

The following pairs are in P≥:

LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0]) → LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))
LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1]))) → COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))

There are no usable rules.

(40) Complex Obligation (AND)

(41) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0]) → LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))
(1): LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1]))) → COND_LOAD1102ARR1(i96[1] > 0 && i96[1] < i3[1] && i98[1] > 0 && i96[1] + 1 > 0, java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))

(0) -> (1), if ((i98[0] →* i98[1])∧((i175[0] →* i175[1])∧(i174[0] →* i174[1])∧(i176[0] →* i176[1])∧(a1572[0] →* a1572[1]))∧((i3[0] →* i3[1])∧(a1201data[0] →* a1201data[1]))∧(i96[0] →* i96[1]))



The set Q consists of the following terms:
Load1102(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load1102ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1102ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

(42) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(43) TRUE

(44) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0]) → LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))
(2): COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2]))) → LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2] + 1, i98[2] + -1)

(2) -> (0), if ((i98[2] + -1 →* i98[0])∧((i3[2] →* i3[0])∧(a1201data[2] →* a1201data[0]))∧(i96[2] + 1 →* i96[0]))



The set Q consists of the following terms:
Load1102(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load1102ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1102ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

(45) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(46) TRUE